/*
 * Copyright 2011 Fabian Wenzelmann
 * 
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 * 
 * Recognition-Procedures-for-Boolean-Functions is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 * 
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 * 
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.  If not, see <http://www.gnu.org/licenses/>.
 */

package de.wenzelmf.booleanFunction.lpb.util;

import java.io.IOException;
import java.io.ObjectInputStream;
import java.io.ObjectOutputStream;
import java.io.Serializable;
import java.util.ArrayList;
import java.util.Collection;
import java.util.Iterator;

import de.wenzelmf.booleanFunction.dnf.Clause;
import de.wenzelmf.booleanFunction.dnf.ClauseFactory;
import de.wenzelmf.booleanFunction.dnf.DNF;
import de.wenzelmf.booleanFunction.dnf.DNFFactory;
import de.wenzelmf.booleanFunction.dnf.Literal;
import de.wenzelmf.booleanFunction.util.Tuple;

/**
 * Class to represent LPBs.
 * 
 * @author Fabian Wenzelmann
 * @version 1.0
 *
 */
public class LPB implements Serializable, Iterable<LPBSummand>
{
	private static final long serialVersionUID = -8631847465819341462L;
	
	/*
	 * Default size for the coefficient list. 
	 */
	protected static final int DEFAULT_SIZE = 8;
	
	/*
	 * Degree of the LPB.
	 */
	private transient int degree;
	
	/*
	 * The summands of the LPB.
	 */
	private transient ArrayList<LPBSummand> summands;

	/**
	 * Constructs new LPB.
	 * 
	 * @param summands All pairs of coefficients and identifiers. 
	 * @param degree The degree of the LPB.
	 */
	public LPB(Collection<LPBSummand> summands, int degree)
	{
		this.summands = new ArrayList<LPBSummand>(summands);
		this.degree = degree;
	}
	
	/**
	 * Constructs new LPB.
	 * 
	 * Nearly the same as #LPB(Collection, int) but no new Array List is created.
	 * So changes to the {@code summands} list are reflected to the summands of the LPB.
	 * 
	 * @param summands All pairs of coefficients and identifiers.
	 * @param degree The degree of the LPB.
	 */
	public LPB(ArrayList<LPBSummand> summands, int degree)
	{
		this.summands = summands;
		this.degree = degree;
	}
	
	/**
	 * Creates new LPB.
	 * 
	 * The summands list is an empty list with capacity for {@code initialSize} many summands.
	 * 
	 * @param degree The degree of the LPB.
	 * @param initialSize The initial size of the Array List used to store the summands.
	 */
	public LPB(int degree, int initialSize)
	{
		this.summands = new ArrayList<LPBSummand>(initialSize);
		this.degree = degree;
	}
	
	/**
	 * Creates a new LPB.
	 * 
	 * The summands list is an empty list.
	 * 
	 * @param degree The degree of the LPB.
	 */
	public LPB(int degree)
	{
		this(degree, DEFAULT_SIZE);
	}
	
	/**
	 * Returns the degree of the LPB, the degree is the <i>d</i> in
	 * a<sub>1</sub>l<sub>1</sub> + &hellip; + a<sub>n</sub>l<sub>n</sub> &ge; d.
	 * 
	 * @return The degree of this LPB.
	 */
	public int getDegree()
	{
		return degree;
	}

	/**
	 * Returns an iterator over all summands of the LPB, i. e. returns the elements
	 * a<sub>i</sub>l<sub>i</sub> for 1 &le; i &le; n.
	 * 
	 * @return An iterator over all summands.
	 */
	@Override
	public Iterator<LPBSummand> iterator()
	{
		return summands.iterator();
	}
	
	/**
	 * Add a new summand to this summands list.
	 * 
	 * Note that if there's already a occurrence with the literal defined in summand, this
	 * summand is added nevertheless. So take care to add for each identifier only one summand.
	 * 
	 * @param summand The summand to add.
	 */
	public void addSummand(LPBSummand summand)
	{
		this.summands.add(summand);
	}
	
	/**
	 * Returns the size of this LPB, i. e. the length of the summands list.
	 * 
	 * @return size of the summands list.
	 */
	public int size()
	{
		return summands.size();
	}
	
	/**
	 * Return the summand from the summands list.
	 * 
	 * @param summand The summand to remove.
	 * 
	 * @return {@code true} if the collection contained the element.
	 */
	public boolean remove(LPBSummand summand)
	{
		return summands.remove(summand);
	}
	
	/**
	 * Return a String representation of this object using {@code geq} as greater-than-or-equal sign.
	 * 
	 * @param geq The String that is used as greater-than-or-equal sign.
	 *  
	 * @return "a<sub>1</sub>l<sub>1</sub> + &hellip; + a<sub>n</sub>l<sub>n</sub> &ge; d" where  &ge;
	 * is the {@code geq} String. 
	 */
	public String toString(String geq)
	{
		StringBuilder result = new StringBuilder();
		boolean first = true;
		if(summands.size() == 0)
			result.append("0 ");
		for(LPBSummand s : summands)
		{
			if(first)
			{
				first = false;
			}
			else
			{
				result.append(" ");
				result.append("+");
				result.append(" ");
			}
			result.append(s);
		}
		if(summands.size() != 0)
			result.append(" ");
		result.append(geq);
		result.append(" ");
		result.append(degree);
		return result.toString();
	}
	
	/**
	 * Returns a String representation of this LPB.
	 * 
	 * Returns {@link #toString(String)} with ">=".
	 * 
	 * @return {@code this.toString(">=")}
	 * @see #toString(String)
	 */
	@Override
	public String toString()
	{
		return toString(">=");
	}
	
	/**
	 * Converts this LPB to a DNF.
	 * 
	 * @param clauseFactory The factory that is used to create new Clause objects.
	 * @param dnfFactory The factory that is used to create new DNF objects.
	 * 
	 * @return A DNF &phi; that represents this LPB.
	 */
	public DNF toDNF(ClauseFactory clauseFactory, DNFFactory dnfFactory)
	{
		int n = size();
		
		if(n == 0 && degree > 0)
			return dnfFactory.getEmptyDNF(0);
		
		if(degree <= 0)
		{
			Clause c = clauseFactory.getEmptyClause(0);
			DNF dnf = dnfFactory.getEmptyDNF(2);
			dnf.add(c);
			return dnf;
		}
		
		DNF dnf = dnfFactory.getEmptyDNF();
		ArrayList<ArrayList<Tuple<Clause, Integer>>> clauseSets = new ArrayList<ArrayList<Tuple<Clause, Integer>>>(n);
		for(int i = 0; i < n; i++)
		{
			Tuple<Clause, Integer> t = new Tuple<Clause, Integer>(clauseFactory.getEmptyClause(), 0);
			// TODO: estimate size?
			ArrayList<Tuple<Clause, Integer>> ci = new ArrayList<Tuple<Clause, Integer>>();
			ci.add(t);
			clauseSets.add(ci);
		}
		
		int i = 0;
		for(LPBSummand s : summands)
		{
			for(Tuple<Clause, Integer> t : clauseSets.get(i))
			{	
				if(s.getCoefficient() + t.getSecond() >= degree)
				{
					t.getFirst().add(s.getLiteral());
					dnf.add(t.getFirst());
				}
				else
				{
					for(int j = i + 1; j < n; j++)
					{
						// we have to create a copy of c
						// TODO: size
						Clause cPrime = clauseFactory.getEmptyClause(2 * t.getFirst().size());
						for(Literal l : t.getFirst())
						{
							cPrime.add(l);
						}
						cPrime.add(s.getLiteral());
						Tuple<Clause, Integer> newT = new Tuple<Clause, Integer>(cPrime, t.getSecond() + s.getCoefficient());
						
						clauseSets.get(j).add(newT);
					}
				}
			}
			i++;
		}
		return dnf;
	}
	
	/**
	 * Converts this LPB to a DNF.
	 * 
	 * Just calls {@link #toDNF(ClauseFactory, DNFFactory)} with the default factories as defined in {@link LPBCombinatorialConstants}.
	 * 
	 * @return A DNF &phi; that represents this LPB.
	 */
	public DNF toDNF()
	{
		return toDNF(LPBCombinatorialConstants.defaultClauseFactory, LPBCombinatorialConstants.defaultDNFFactory);
	}
	
	private void writeObject(ObjectOutputStream out) throws IOException
	{
		out.defaultWriteObject();
		// write degree
		out.writeInt(degree);
		// write summands size
		out.writeInt(summands.size());
		// write all summands
		for(LPBSummand s : summands)
		{
			out.writeObject(s);
		}
	}
	
	private void readObject(ObjectInputStream in) throws IOException, ClassNotFoundException
	{
		// first read the degree
		this.degree = in.readInt();
		// read summands
		int size = in.readInt();
		// create list and read all summands
		this.summands = new ArrayList<LPBSummand>(size);
		for(int i = 0; i < size; i++)
		{
			// TODO: is this ok so?
			summands.add((LPBSummand)in.readObject());
		}
	}
	
}